;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "mborder.lisp")
(require "mbmptree.lisp")
(require "mavltree.lisp")
(require "mdatagenerators.lisp")
(require "mcrop.lisp")

(module Tborder
  (import Iborder)
  (import Ibmptree)
  (import Iavltree)
  (import IDataGenerators)
  (import ICrop)
  
  (include-book "doublecheck" :dir :teachpacks) 
  (include-book "testing" :dir :teachpacks)
  
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ; DATA GENERATORS
  ; Generates a random pixel (random RGB values).
  (defrandom random-pixel ()
    (let* ((r (random-between 0 255))
           (g (random-between 0 255))
           (b (random-between 0 255)))
      (list r g b)))
 
  ; Random bitmap file, uses a static header with a 
  ; size of heightxwidth.
  (defrandom random-bitmap (height width)
    (let* ((header (list 66 77 54 12 0 0 0 0 0 0 54 0 0 
                         0 40 0 0 0 width 0 0 0 height 0 0 0 1 
                         0 24 0 0 0 0 0 0 12 0 0 0 0 0 
                         0 0 0 0 0 0 0 0 0 0 0 0 0))
           (pixels (random-list-of (random-pixel) :size (* width height)))
           (tr (insert-header (empty-bmp-tree) header)))
      (fill-bitmap tr 0 0 height width pixels)))

  
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defproperty border-changes-bitmap :repeat 10
  (h          :value (random-between 1 20)
   w          :value (random-between 1 20)
   thickness  :value (random-between 1 5)
   r          :value (random-between 0 255)
   g          :value (random-between 0 255)
   b          :value (random-between 0 255)
   bmp        :value (random-bitmap h w)
   border-bmp :value (border bmp thickness r g b))
  (not (equal bmp border-bmp)))
  
  (defproperty crop-removes-border :repeat 10
    (h          :value (random-between 1 20)
     w          :value (random-between 1 20)
     thickness  :value (random-between 1 5)
     r          :value (random-between 0 255)
     g          :value (random-between 0 255)
     b          :value (random-between 0 255)
     bmp        :value (random-bitmap h w)
     border-bmp :value (border bmp thickness r g b)
     crop-bmp   :value (crop border-bmp thickness thickness (- (+ h thickness) 1) (- (+ w thickness) 1)))
    (equal (cdr (bmp-flatten bmp)) (cdr (bmp-flatten crop-bmp))))
  
  (defproperty border-adds-solid-color-to-left-of-bitmap :repeat 10
    (h          :value (random-between 1 20)
     w          :value (random-between 1 20)
     thickness  :value (random-between 1 5)
     r          :value (random-between 0 255)
     g          :value (random-between 0 255)
     b          :value (random-between 0 255)
     bmp        :value (random-bitmap h w)
     border-bmp :value (border bmp thickness r g b)
     crop-bmp   :value (crop border-bmp 0 0 (- (+ (* 2 thickness) h) 1) (- thickness 1))
     solid-color :value (make-solid-color-image (+ h (* 2 thickness)) thickness r g b))
    (equal (cdr (bmp-flatten solid-color)) (cdr (bmp-flatten crop-bmp))))
  
  (defproperty border-adds-solid-color-to-right-of-bitmap :repeat 10
    (h          :value (random-between 1 20)
     w          :value (random-between 1 20)
     thickness  :value (random-between 1 5)
     r          :value (random-between 0 255)
     g          :value (random-between 0 255)
     b          :value (random-between 0 255)
     bmp        :value (random-bitmap h w)
     border-bmp :value (border bmp thickness r g b)
     crop-bmp   :value (crop border-bmp 0 (+ thickness w) (- (+ (* 2 thickness) h) 1) (- (+ (* 2 thickness) w) 1))
     solid-color :value (make-solid-color-image (+ h (* 2 thickness)) thickness r g b))
    (equal (cdr (bmp-flatten solid-color)) (cdr (bmp-flatten crop-bmp))))
  
  (defproperty border-adds-solid-color-to-top-of-bitmap :repeat 10
    (h          :value (random-between 1 20)
     w          :value (random-between 1 20)
     thickness  :value (random-between 1 5)
     r          :value (random-between 0 255)
     g          :value (random-between 0 255)
     b          :value (random-between 0 255)
     bmp        :value (random-bitmap h w)
     border-bmp :value (border bmp thickness r g b)
     crop-bmp   :value (crop border-bmp 0 0 (- thickness 1) (- (+ (* 2 thickness) w) 1))
     solid-color :value (make-solid-color-image thickness (+ w (* 2 thickness)) r g b))
    (equal (cdr (bmp-flatten solid-color)) (cdr (bmp-flatten crop-bmp))))
  
  (defproperty border-adds-solid-color-to-bottom-of-bitmap :repeat 10
    (h          :value (random-between 1 20)
     w          :value (random-between 1 20)
     thickness  :value (random-between 1 5)
     r          :value (random-between 0 255)
     g          :value (random-between 0 255)
     b          :value (random-between 0 255)
     bmp        :value (random-bitmap h w)
     border-bmp :value (border bmp thickness r g b)
     crop-bmp   :value (crop border-bmp (+ thickness h) 0 (- (+ (* 2 thickness) h) 1) (- (+ (* 2 thickness) w) 1))
     solid-color :value (make-solid-color-image thickness (+ w (* 2 thickness)) r g b))
    (equal (cdr (bmp-flatten solid-color)) (cdr (bmp-flatten crop-bmp))))
)
(link RTborder (Mavltree Mbmptree MDataGenerators Mborder MCrop Tborder))
(invoke RTborder)